Termination w.r.t. Q proof of /tmp/tmpVymCOQ/Ex3_2_Luc97

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ACTIVE(dbls(cons(X, Y))) → DBLS(Y)
FROM(mark(X)) → FROM(X)
ACTIVE(dbls(cons(X, Y))) → MARK(cons(dbl(X), dbls(Y)))
MARK(indx(X1, X2)) → MARK(X1)
FROM(active(X)) → FROM(X)
CONS(X1, mark(X2)) → CONS(X1, X2)
ACTIVE(indx(cons(X, Y), Z)) → SEL(X, Z)
DBL(active(X)) → DBL(X)
DBL(mark(X)) → DBL(X)
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(indx(X1, X2)) → INDX(mark(X1), X2)
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(dbls(X)) → ACTIVE(dbls(mark(X)))
MARK(sel(X1, X2)) → MARK(X1)
S(active(X)) → S(X)
ACTIVE(dbls(nil)) → MARK(nil)
DBLS(active(X)) → DBLS(X)
MARK(dbl(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(X))
INDX(mark(X1), X2) → INDX(X1, X2)
ACTIVE(dbl(s(X))) → DBL(X)
ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X))))
CONS(active(X1), X2) → CONS(X1, X2)
MARK(indx(X1, X2)) → ACTIVE(indx(mark(X1), X2))
MARK(cons(X1, X2)) → ACTIVE(cons(X1, X2))
INDX(X1, mark(X2)) → INDX(X1, X2)
ACTIVE(dbls(cons(X, Y))) → DBL(X)
ACTIVE(from(X)) → FROM(s(X))
ACTIVE(dbl(s(X))) → S(dbl(X))
SEL(mark(X1), X2) → SEL(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
ACTIVE(dbl(0)) → MARK(0)
SEL(X1, active(X2)) → SEL(X1, X2)
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
CONS(X1, active(X2)) → CONS(X1, X2)
MARK(dbls(X)) → DBLS(mark(X))
ACTIVE(indx(cons(X, Y), Z)) → INDX(Y, Z)
SEL(X1, mark(X2)) → SEL(X1, X2)
SEL(active(X1), X2) → SEL(X1, X2)
INDX(X1, active(X2)) → INDX(X1, X2)
ACTIVE(dbls(cons(X, Y))) → CONS(dbl(X), dbls(Y))
MARK(dbl(X)) → DBL(mark(X))
DBLS(mark(X)) → DBLS(X)
S(mark(X)) → S(X)
ACTIVE(indx(cons(X, Y), Z)) → CONS(sel(X, Z), indx(Y, Z))
ACTIVE(dbl(s(X))) → S(s(dbl(X)))
INDX(active(X1), X2) → INDX(X1, X2)
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
ACTIVE(from(X)) → S(X)
MARK(dbl(X)) → ACTIVE(dbl(mark(X)))
MARK(sel(X1, X2)) → SEL(mark(X1), mark(X2))
MARK(0) → ACTIVE(0)
MARK(from(X)) → ACTIVE(from(X))
ACTIVE(indx(nil, X)) → MARK(nil)
ACTIVE(sel(s(X), cons(Y, Z))) → SEL(X, Z)
MARK(nil) → ACTIVE(nil)
ACTIVE(from(X)) → CONS(X, from(s(X)))
MARK(sel(X1, X2)) → MARK(X2)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(dbls(cons(X, Y))) → DBLS(Y)
FROM(mark(X)) → FROM(X)
ACTIVE(dbls(cons(X, Y))) → MARK(cons(dbl(X), dbls(Y)))
MARK(indx(X1, X2)) → MARK(X1)
FROM(active(X)) → FROM(X)
CONS(X1, mark(X2)) → CONS(X1, X2)
ACTIVE(indx(cons(X, Y), Z)) → SEL(X, Z)
DBL(active(X)) → DBL(X)
DBL(mark(X)) → DBL(X)
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(indx(X1, X2)) → INDX(mark(X1), X2)
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(dbls(X)) → ACTIVE(dbls(mark(X)))
MARK(sel(X1, X2)) → MARK(X1)
S(active(X)) → S(X)
ACTIVE(dbls(nil)) → MARK(nil)
DBLS(active(X)) → DBLS(X)
MARK(dbl(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(X))
INDX(mark(X1), X2) → INDX(X1, X2)
ACTIVE(dbl(s(X))) → DBL(X)
ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X))))
CONS(active(X1), X2) → CONS(X1, X2)
MARK(indx(X1, X2)) → ACTIVE(indx(mark(X1), X2))
MARK(cons(X1, X2)) → ACTIVE(cons(X1, X2))
INDX(X1, mark(X2)) → INDX(X1, X2)
ACTIVE(dbls(cons(X, Y))) → DBL(X)
ACTIVE(from(X)) → FROM(s(X))
ACTIVE(dbl(s(X))) → S(dbl(X))
SEL(mark(X1), X2) → SEL(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
ACTIVE(dbl(0)) → MARK(0)
SEL(X1, active(X2)) → SEL(X1, X2)
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
CONS(X1, active(X2)) → CONS(X1, X2)
MARK(dbls(X)) → DBLS(mark(X))
ACTIVE(indx(cons(X, Y), Z)) → INDX(Y, Z)
SEL(X1, mark(X2)) → SEL(X1, X2)
SEL(active(X1), X2) → SEL(X1, X2)
INDX(X1, active(X2)) → INDX(X1, X2)
ACTIVE(dbls(cons(X, Y))) → CONS(dbl(X), dbls(Y))
MARK(dbl(X)) → DBL(mark(X))
DBLS(mark(X)) → DBLS(X)
S(mark(X)) → S(X)
ACTIVE(indx(cons(X, Y), Z)) → CONS(sel(X, Z), indx(Y, Z))
ACTIVE(dbl(s(X))) → S(s(dbl(X)))
INDX(active(X1), X2) → INDX(X1, X2)
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
ACTIVE(from(X)) → S(X)
MARK(dbl(X)) → ACTIVE(dbl(mark(X)))
MARK(sel(X1, X2)) → SEL(mark(X1), mark(X2))
MARK(0) → ACTIVE(0)
MARK(from(X)) → ACTIVE(from(X))
ACTIVE(indx(nil, X)) → MARK(nil)
ACTIVE(sel(s(X), cons(Y, Z))) → SEL(X, Z)
MARK(nil) → ACTIVE(nil)
ACTIVE(from(X)) → CONS(X, from(s(X)))
MARK(sel(X1, X2)) → MARK(X2)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 8 SCCs with 22 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FROM(mark(X)) → FROM(X)
FROM(active(X)) → FROM(X)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FROM(mark(X)) → FROM(X)
FROM(active(X)) → FROM(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

FROM(mark(X)) → FROM(X)
The graph contains the following edges 1 > 1
FROM(active(X)) → FROM(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INDX(X1, active(X2)) → INDX(X1, X2)
INDX(active(X1), X2) → INDX(X1, X2)
INDX(mark(X1), X2) → INDX(X1, X2)
INDX(X1, mark(X2)) → INDX(X1, X2)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INDX(active(X1), X2) → INDX(X1, X2)
INDX(X1, active(X2)) → INDX(X1, X2)
INDX(mark(X1), X2) → INDX(X1, X2)
INDX(X1, mark(X2)) → INDX(X1, X2)

From the DPs we obtained the following set of size-change graphs:

INDX(X1, active(X2)) → INDX(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
INDX(active(X1), X2) → INDX(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
INDX(mark(X1), X2) → INDX(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
INDX(X1, mark(X2)) → INDX(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SEL(mark(X1), X2) → SEL(X1, X2)
SEL(X1, active(X2)) → SEL(X1, X2)
SEL(X1, mark(X2)) → SEL(X1, X2)
SEL(active(X1), X2) → SEL(X1, X2)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SEL(mark(X1), X2) → SEL(X1, X2)
SEL(X1, active(X2)) → SEL(X1, X2)
SEL(X1, mark(X2)) → SEL(X1, X2)
SEL(active(X1), X2) → SEL(X1, X2)

From the DPs we obtained the following set of size-change graphs:

SEL(mark(X1), X2) → SEL(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
SEL(X1, active(X2)) → SEL(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
SEL(X1, mark(X2)) → SEL(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
SEL(active(X1), X2) → SEL(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONS(X1, active(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONS(mark(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)

From the DPs we obtained the following set of size-change graphs:

CONS(X1, active(X2)) → CONS(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
CONS(mark(X1), X2) → CONS(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
CONS(active(X1), X2) → CONS(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
CONS(X1, mark(X2)) → CONS(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DBLS(mark(X)) → DBLS(X)
DBLS(active(X)) → DBLS(X)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DBLS(mark(X)) → DBLS(X)
DBLS(active(X)) → DBLS(X)

From the DPs we obtained the following set of size-change graphs:

DBLS(mark(X)) → DBLS(X)
The graph contains the following edges 1 > 1
DBLS(active(X)) → DBLS(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(mark(X)) → S(X)
S(active(X)) → S(X)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(active(X)) → S(X)
S(mark(X)) → S(X)

From the DPs we obtained the following set of size-change graphs:

S(mark(X)) → S(X)
The graph contains the following edges 1 > 1
S(active(X)) → S(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DBL(mark(X)) → DBL(X)
DBL(active(X)) → DBL(X)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DBL(mark(X)) → DBL(X)
DBL(active(X)) → DBL(X)

From the DPs we obtained the following set of size-change graphs:

DBL(mark(X)) → DBL(X)
The graph contains the following edges 1 > 1
DBL(active(X)) → DBL(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(sel(X1, X2)) → MARK(X1)
ACTIVE(dbls(cons(X, Y))) → MARK(cons(dbl(X), dbls(Y)))
MARK(indx(X1, X2)) → MARK(X1)
MARK(dbl(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(X))
MARK(dbls(X)) → MARK(X)
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
MARK(dbl(X)) → ACTIVE(dbl(mark(X)))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X))))
MARK(from(X)) → ACTIVE(from(X))
MARK(indx(X1, X2)) → ACTIVE(indx(mark(X1), X2))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
MARK(cons(X1, X2)) → ACTIVE(cons(X1, X2))
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(sel(X1, X2)) → MARK(X2)
MARK(dbls(X)) → ACTIVE(dbls(mark(X)))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(s(X)) → ACTIVE(s(X))
MARK(cons(X1, X2)) → ACTIVE(cons(X1, X2))

The remaining pairs can at least be oriented weakly.

MARK(sel(X1, X2)) → MARK(X1)
ACTIVE(dbls(cons(X, Y))) → MARK(cons(dbl(X), dbls(Y)))
MARK(indx(X1, X2)) → MARK(X1)
MARK(dbl(X)) → MARK(X)
MARK(dbls(X)) → MARK(X)
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
MARK(dbl(X)) → ACTIVE(dbl(mark(X)))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X))))
MARK(from(X)) → ACTIVE(from(X))
MARK(indx(X1, X2)) → ACTIVE(indx(mark(X1), X2))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(sel(X1, X2)) → MARK(X2)
MARK(dbls(X)) → ACTIVE(dbls(mark(X)))

Used ordering: Matrix interpretation [3]:
Non-tuple symbols:

M( sel(x₁, x₂) ) =

/	0	\
\	1	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( indx(x₁, x₂) ) =

/	0	\
\	1	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( cons(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( active(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( from(x₁) ) =

/	0	\
\	1	/

/	0	0	\
\	0	0	/

x₁

M( dbl(x₁) ) =

/	0	\
\	1	/

/	0	0	\
\	0	0	/

x₁

M( mark(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( s(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( dbls(x₁) ) =

/	0	\
\	1	/

/	0	0	\
\	0	0	/

x₁

M( 0 ) =

/	0	\
\	0	/

M( nil ) =

/	0	\
\	0	/

Tuple symbols:

M( MARK(x₁) ) =

[

]

x₁

M( ACTIVE(x₁) ) =

[

]

x₁

Matrix type:
We used a basic matrix type which is not further parametrizeable.

As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:

cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
indx(X1, mark(X2)) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
from(active(X)) → from(X)
from(mark(X)) → from(X)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(sel(X1, X2)) → MARK(X1)
ACTIVE(dbls(cons(X, Y))) → MARK(cons(dbl(X), dbls(Y)))
MARK(indx(X1, X2)) → MARK(X1)
MARK(dbl(X)) → MARK(X)
MARK(dbls(X)) → MARK(X)
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
MARK(dbl(X)) → ACTIVE(dbl(mark(X)))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X))))
MARK(from(X)) → ACTIVE(from(X))
MARK(indx(X1, X2)) → ACTIVE(indx(mark(X1), X2))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(dbls(X)) → ACTIVE(dbls(mark(X)))
MARK(sel(X1, X2)) → MARK(X2)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVE(dbls(cons(X, Y))) → MARK(cons(dbl(X), dbls(Y))) at position [0] we obtained the following new rules:

ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(sel(X1, X2)) → MARK(X1)
MARK(indx(X1, X2)) → MARK(X1)
MARK(dbl(X)) → MARK(X)
MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2)))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(dbl(X)) → ACTIVE(dbl(mark(X)))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X))))
MARK(from(X)) → ACTIVE(from(X))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
MARK(indx(X1, X2)) → ACTIVE(indx(mark(X1), X2))
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(sel(X1, X2)) → MARK(X2)
MARK(dbls(X)) → ACTIVE(dbls(mark(X)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(sel(X1, X2)) → ACTIVE(sel(mark(X1), mark(X2))) at position [0] we obtained the following new rules:

MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(dbls(X)) → ACTIVE(dbls(mark(X)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(dbl(X)) → MARK(X)
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(dbl(X)) → ACTIVE(dbl(mark(X)))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X))))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(from(X)) → ACTIVE(from(X))
MARK(indx(X1, X2)) → ACTIVE(indx(mark(X1), X2))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(sel(X1, X2)) → MARK(X2)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(dbl(X)) → ACTIVE(dbl(mark(X))) at position [0] we obtained the following new rules:

MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
MARK(dbl(0)) → ACTIVE(dbl(active(0)))
MARK(dbl(nil)) → ACTIVE(dbl(active(nil)))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbl(0)) → ACTIVE(dbl(active(0)))
MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
MARK(dbl(nil)) → ACTIVE(dbl(active(nil)))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(dbls(X)) → ACTIVE(dbls(mark(X)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(dbl(X)) → MARK(X)
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X))))
MARK(from(X)) → ACTIVE(from(X))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(indx(X1, X2)) → ACTIVE(indx(mark(X1), X2))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(sel(X1, X2)) → MARK(X2)

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X)))) at position [0] we obtained the following new rules:

ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(dbls(X)) → ACTIVE(dbls(mark(X)))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(dbl(X)) → MARK(X)
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(indx(X1, X2)) → ACTIVE(indx(mark(X1), X2))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbl(0)) → ACTIVE(dbl(active(0)))
ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(dbl(nil)) → ACTIVE(dbl(active(nil)))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(from(X)) → ACTIVE(from(X))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(indx(X1, X2)) → ACTIVE(indx(mark(X1), X2)) at position [0] we obtained the following new rules:

MARK(indx(s(x0), y1)) → ACTIVE(indx(active(s(x0)), y1))
MARK(indx(indx(x0, x1), y1)) → ACTIVE(indx(active(indx(mark(x0), x1)), y1))
MARK(indx(cons(x0, x1), y1)) → ACTIVE(indx(active(cons(x0, x1)), y1))
MARK(indx(from(x0), y1)) → ACTIVE(indx(active(from(x0)), y1))
MARK(indx(sel(x0, x1), y1)) → ACTIVE(indx(active(sel(mark(x0), mark(x1))), y1))
MARK(indx(nil, y1)) → ACTIVE(indx(active(nil), y1))
MARK(indx(y0, mark(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(dbl(x0), y1)) → ACTIVE(indx(active(dbl(mark(x0))), y1))
MARK(indx(y0, active(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(0, y1)) → ACTIVE(indx(active(0), y1))
MARK(indx(x0, x1)) → ACTIVE(indx(x0, x1))
MARK(indx(dbls(x0), y1)) → ACTIVE(indx(active(dbls(mark(x0))), y1))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(indx(nil, y1)) → ACTIVE(indx(active(nil), y1))
MARK(indx(s(x0), y1)) → ACTIVE(indx(active(s(x0)), y1))
MARK(indx(indx(x0, x1), y1)) → ACTIVE(indx(active(indx(mark(x0), x1)), y1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
MARK(indx(dbl(x0), y1)) → ACTIVE(indx(active(dbl(mark(x0))), y1))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(indx(x0, x1)) → ACTIVE(indx(x0, x1))
MARK(dbls(X)) → ACTIVE(dbls(mark(X)))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(indx(from(x0), y1)) → ACTIVE(indx(active(from(x0)), y1))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(indx(sel(x0, x1), y1)) → ACTIVE(indx(active(sel(mark(x0), mark(x1))), y1))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(dbl(X)) → MARK(X)
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbl(0)) → ACTIVE(dbl(active(0)))
ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
MARK(indx(dbls(x0), y1)) → ACTIVE(indx(active(dbls(mark(x0))), y1))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(dbl(nil)) → ACTIVE(dbl(active(nil)))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(indx(y0, mark(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(indx(0, y1)) → ACTIVE(indx(active(0), y1))
MARK(indx(y0, active(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(cons(x0, x1), y1)) → ACTIVE(indx(active(cons(x0, x1)), y1))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(from(X)) → ACTIVE(from(X))
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(dbls(X)) → ACTIVE(dbls(mark(X))) at position [0] we obtained the following new rules:

MARK(dbls(indx(x0, x1))) → ACTIVE(dbls(active(indx(mark(x0), x1))))
MARK(dbls(s(x0))) → ACTIVE(dbls(active(s(x0))))
MARK(dbls(from(x0))) → ACTIVE(dbls(active(from(x0))))
MARK(dbls(dbls(x0))) → ACTIVE(dbls(active(dbls(mark(x0)))))
MARK(dbls(dbl(x0))) → ACTIVE(dbls(active(dbl(mark(x0)))))
MARK(dbls(nil)) → ACTIVE(dbls(active(nil)))
MARK(dbls(sel(x0, x1))) → ACTIVE(dbls(active(sel(mark(x0), mark(x1)))))
MARK(dbls(0)) → ACTIVE(dbls(active(0)))
MARK(dbls(cons(x0, x1))) → ACTIVE(dbls(active(cons(x0, x1))))
MARK(dbls(x0)) → ACTIVE(dbls(x0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(indx(nil, y1)) → ACTIVE(indx(active(nil), y1))
MARK(indx(s(x0), y1)) → ACTIVE(indx(active(s(x0)), y1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(indx(indx(x0, x1), y1)) → ACTIVE(indx(active(indx(mark(x0), x1)), y1))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
MARK(indx(dbl(x0), y1)) → ACTIVE(indx(active(dbl(mark(x0))), y1))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(indx(x0, x1)) → ACTIVE(indx(x0, x1))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(dbls(indx(x0, x1))) → ACTIVE(dbls(active(indx(mark(x0), x1))))
MARK(sel(X1, X2)) → MARK(X1)
MARK(indx(from(x0), y1)) → ACTIVE(indx(active(from(x0)), y1))
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(indx(sel(x0, x1), y1)) → ACTIVE(indx(active(sel(mark(x0), mark(x1))), y1))
MARK(dbl(X)) → MARK(X)
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(dbls(sel(x0, x1))) → ACTIVE(dbls(active(sel(mark(x0), mark(x1)))))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbls(from(x0))) → ACTIVE(dbls(active(from(x0))))
MARK(dbl(0)) → ACTIVE(dbl(active(0)))
MARK(dbls(dbl(x0))) → ACTIVE(dbls(active(dbl(mark(x0)))))
ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
MARK(dbls(0)) → ACTIVE(dbls(active(0)))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(x0)) → ACTIVE(dbls(x0))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(indx(dbls(x0), y1)) → ACTIVE(indx(active(dbls(mark(x0))), y1))
MARK(dbls(s(x0))) → ACTIVE(dbls(active(s(x0))))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(dbl(nil)) → ACTIVE(dbl(active(nil)))
MARK(dbls(nil)) → ACTIVE(dbls(active(nil)))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(indx(y0, mark(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(y0, active(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(0, y1)) → ACTIVE(indx(active(0), y1))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(indx(cons(x0, x1), y1)) → ACTIVE(indx(active(cons(x0, x1)), y1))
MARK(dbls(dbls(x0))) → ACTIVE(dbls(active(dbls(mark(x0)))))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(from(X)) → ACTIVE(from(X))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(dbls(cons(x0, x1))) → ACTIVE(dbls(active(cons(x0, x1))))
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(dbl(0)) → ACTIVE(dbl(active(0))) at position [0] we obtained the following new rules:

MARK(dbl(0)) → ACTIVE(dbl(0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(indx(nil, y1)) → ACTIVE(indx(active(nil), y1))
MARK(dbl(0)) → ACTIVE(dbl(0))
MARK(indx(s(x0), y1)) → ACTIVE(indx(active(s(x0)), y1))
MARK(indx(indx(x0, x1), y1)) → ACTIVE(indx(active(indx(mark(x0), x1)), y1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
MARK(indx(dbl(x0), y1)) → ACTIVE(indx(active(dbl(mark(x0))), y1))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(indx(x0, x1)) → ACTIVE(indx(x0, x1))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(dbls(indx(x0, x1))) → ACTIVE(dbls(active(indx(mark(x0), x1))))
MARK(indx(from(x0), y1)) → ACTIVE(indx(active(from(x0)), y1))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(indx(sel(x0, x1), y1)) → ACTIVE(indx(active(sel(mark(x0), mark(x1))), y1))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(dbl(X)) → MARK(X)
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(dbls(sel(x0, x1))) → ACTIVE(dbls(active(sel(mark(x0), mark(x1)))))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbls(from(x0))) → ACTIVE(dbls(active(from(x0))))
MARK(dbls(dbl(x0))) → ACTIVE(dbls(active(dbl(mark(x0)))))
ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbls(0)) → ACTIVE(dbls(active(0)))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(x0)) → ACTIVE(dbls(x0))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
MARK(indx(dbls(x0), y1)) → ACTIVE(indx(active(dbls(mark(x0))), y1))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(dbls(s(x0))) → ACTIVE(dbls(active(s(x0))))
MARK(dbl(nil)) → ACTIVE(dbl(active(nil)))
MARK(dbls(nil)) → ACTIVE(dbls(active(nil)))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(indx(y0, mark(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(indx(0, y1)) → ACTIVE(indx(active(0), y1))
MARK(indx(y0, active(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(cons(x0, x1), y1)) → ACTIVE(indx(active(cons(x0, x1)), y1))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(dbls(dbls(x0))) → ACTIVE(dbls(active(dbls(mark(x0)))))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(from(X)) → ACTIVE(from(X))
MARK(dbls(cons(x0, x1))) → ACTIVE(dbls(active(cons(x0, x1))))
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

                                              ↳ QDP

                                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(indx(nil, y1)) → ACTIVE(indx(active(nil), y1))
MARK(indx(s(x0), y1)) → ACTIVE(indx(active(s(x0)), y1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(indx(indx(x0, x1), y1)) → ACTIVE(indx(active(indx(mark(x0), x1)), y1))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
MARK(indx(dbl(x0), y1)) → ACTIVE(indx(active(dbl(mark(x0))), y1))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(indx(x0, x1)) → ACTIVE(indx(x0, x1))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(dbls(indx(x0, x1))) → ACTIVE(dbls(active(indx(mark(x0), x1))))
MARK(sel(X1, X2)) → MARK(X1)
MARK(indx(from(x0), y1)) → ACTIVE(indx(active(from(x0)), y1))
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(indx(sel(x0, x1), y1)) → ACTIVE(indx(active(sel(mark(x0), mark(x1))), y1))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(dbl(X)) → MARK(X)
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(dbls(sel(x0, x1))) → ACTIVE(dbls(active(sel(mark(x0), mark(x1)))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbls(from(x0))) → ACTIVE(dbls(active(from(x0))))
MARK(dbls(dbl(x0))) → ACTIVE(dbls(active(dbl(mark(x0)))))
ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
MARK(dbls(0)) → ACTIVE(dbls(active(0)))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(x0)) → ACTIVE(dbls(x0))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
MARK(indx(dbls(x0), y1)) → ACTIVE(indx(active(dbls(mark(x0))), y1))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(dbls(s(x0))) → ACTIVE(dbls(active(s(x0))))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(dbl(nil)) → ACTIVE(dbl(active(nil)))
MARK(dbls(nil)) → ACTIVE(dbls(active(nil)))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(indx(y0, mark(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(indx(0, y1)) → ACTIVE(indx(active(0), y1))
MARK(indx(y0, active(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(indx(cons(x0, x1), y1)) → ACTIVE(indx(active(cons(x0, x1)), y1))
MARK(dbls(dbls(x0))) → ACTIVE(dbls(active(dbls(mark(x0)))))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(from(X)) → ACTIVE(from(X))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(dbls(cons(x0, x1))) → ACTIVE(dbls(active(cons(x0, x1))))
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(dbl(nil)) → ACTIVE(dbl(active(nil))) at position [0] we obtained the following new rules:

MARK(dbl(nil)) → ACTIVE(dbl(nil))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(indx(nil, y1)) → ACTIVE(indx(active(nil), y1))
MARK(indx(s(x0), y1)) → ACTIVE(indx(active(s(x0)), y1))
MARK(indx(indx(x0, x1), y1)) → ACTIVE(indx(active(indx(mark(x0), x1)), y1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(indx(dbl(x0), y1)) → ACTIVE(indx(active(dbl(mark(x0))), y1))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(indx(x0, x1)) → ACTIVE(indx(x0, x1))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(dbls(indx(x0, x1))) → ACTIVE(dbls(active(indx(mark(x0), x1))))
MARK(indx(from(x0), y1)) → ACTIVE(indx(active(from(x0)), y1))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(indx(sel(x0, x1), y1)) → ACTIVE(indx(active(sel(mark(x0), mark(x1))), y1))
MARK(dbl(X)) → MARK(X)
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(dbls(sel(x0, x1))) → ACTIVE(dbls(active(sel(mark(x0), mark(x1)))))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbls(from(x0))) → ACTIVE(dbls(active(from(x0))))
MARK(dbls(dbl(x0))) → ACTIVE(dbls(active(dbl(mark(x0)))))
ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbls(0)) → ACTIVE(dbls(active(0)))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(x0)) → ACTIVE(dbls(x0))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(indx(dbls(x0), y1)) → ACTIVE(indx(active(dbls(mark(x0))), y1))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(dbls(s(x0))) → ACTIVE(dbls(active(s(x0))))
MARK(dbls(nil)) → ACTIVE(dbls(active(nil)))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(indx(y0, mark(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(y0, active(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(0, y1)) → ACTIVE(indx(active(0), y1))
MARK(indx(cons(x0, x1), y1)) → ACTIVE(indx(active(cons(x0, x1)), y1))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(dbls(dbls(x0))) → ACTIVE(dbls(active(dbls(mark(x0)))))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(from(X)) → ACTIVE(from(X))
MARK(dbls(cons(x0, x1))) → ACTIVE(dbls(active(cons(x0, x1))))
MARK(dbl(nil)) → ACTIVE(dbl(nil))
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ DependencyGraphProof

                                                      ↳ QDP

                                                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(indx(nil, y1)) → ACTIVE(indx(active(nil), y1))
MARK(indx(s(x0), y1)) → ACTIVE(indx(active(s(x0)), y1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(indx(indx(x0, x1), y1)) → ACTIVE(indx(active(indx(mark(x0), x1)), y1))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
MARK(indx(dbl(x0), y1)) → ACTIVE(indx(active(dbl(mark(x0))), y1))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(indx(x0, x1)) → ACTIVE(indx(x0, x1))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(dbls(indx(x0, x1))) → ACTIVE(dbls(active(indx(mark(x0), x1))))
MARK(sel(X1, X2)) → MARK(X1)
MARK(indx(from(x0), y1)) → ACTIVE(indx(active(from(x0)), y1))
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(indx(sel(x0, x1), y1)) → ACTIVE(indx(active(sel(mark(x0), mark(x1))), y1))
MARK(dbl(X)) → MARK(X)
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(dbls(sel(x0, x1))) → ACTIVE(dbls(active(sel(mark(x0), mark(x1)))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbls(from(x0))) → ACTIVE(dbls(active(from(x0))))
MARK(dbls(dbl(x0))) → ACTIVE(dbls(active(dbl(mark(x0)))))
ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
MARK(dbls(0)) → ACTIVE(dbls(active(0)))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(x0)) → ACTIVE(dbls(x0))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
MARK(indx(dbls(x0), y1)) → ACTIVE(indx(active(dbls(mark(x0))), y1))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(dbls(s(x0))) → ACTIVE(dbls(active(s(x0))))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(dbls(nil)) → ACTIVE(dbls(active(nil)))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(indx(y0, mark(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(indx(0, y1)) → ACTIVE(indx(active(0), y1))
MARK(indx(y0, active(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(indx(cons(x0, x1), y1)) → ACTIVE(indx(active(cons(x0, x1)), y1))
MARK(dbls(dbls(x0))) → ACTIVE(dbls(active(dbls(mark(x0)))))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(from(X)) → ACTIVE(from(X))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(dbls(cons(x0, x1))) → ACTIVE(dbls(active(cons(x0, x1))))
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(dbls(nil)) → ACTIVE(dbls(active(nil))) at position [0] we obtained the following new rules:

MARK(dbls(nil)) → ACTIVE(dbls(nil))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ DependencyGraphProof

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(indx(nil, y1)) → ACTIVE(indx(active(nil), y1))
MARK(indx(s(x0), y1)) → ACTIVE(indx(active(s(x0)), y1))
MARK(indx(indx(x0, x1), y1)) → ACTIVE(indx(active(indx(mark(x0), x1)), y1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(indx(dbl(x0), y1)) → ACTIVE(indx(active(dbl(mark(x0))), y1))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(indx(x0, x1)) → ACTIVE(indx(x0, x1))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(dbls(indx(x0, x1))) → ACTIVE(dbls(active(indx(mark(x0), x1))))
MARK(indx(from(x0), y1)) → ACTIVE(indx(active(from(x0)), y1))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(indx(sel(x0, x1), y1)) → ACTIVE(indx(active(sel(mark(x0), mark(x1))), y1))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(dbl(X)) → MARK(X)
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(dbls(sel(x0, x1))) → ACTIVE(dbls(active(sel(mark(x0), mark(x1)))))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbls(from(x0))) → ACTIVE(dbls(active(from(x0))))
MARK(dbls(dbl(x0))) → ACTIVE(dbls(active(dbl(mark(x0)))))
ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbls(0)) → ACTIVE(dbls(active(0)))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(x0)) → ACTIVE(dbls(x0))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(indx(dbls(x0), y1)) → ACTIVE(indx(active(dbls(mark(x0))), y1))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(dbls(s(x0))) → ACTIVE(dbls(active(s(x0))))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(indx(y0, mark(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(y0, active(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(0, y1)) → ACTIVE(indx(active(0), y1))
MARK(dbls(nil)) → ACTIVE(dbls(nil))
MARK(indx(cons(x0, x1), y1)) → ACTIVE(indx(active(cons(x0, x1)), y1))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(dbls(dbls(x0))) → ACTIVE(dbls(active(dbls(mark(x0)))))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(from(X)) → ACTIVE(from(X))
MARK(dbls(cons(x0, x1))) → ACTIVE(dbls(active(cons(x0, x1))))
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ DependencyGraphProof

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(indx(nil, y1)) → ACTIVE(indx(active(nil), y1))
MARK(indx(s(x0), y1)) → ACTIVE(indx(active(s(x0)), y1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(indx(indx(x0, x1), y1)) → ACTIVE(indx(active(indx(mark(x0), x1)), y1))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
MARK(indx(dbl(x0), y1)) → ACTIVE(indx(active(dbl(mark(x0))), y1))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(indx(x0, x1)) → ACTIVE(indx(x0, x1))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(dbls(indx(x0, x1))) → ACTIVE(dbls(active(indx(mark(x0), x1))))
MARK(sel(X1, X2)) → MARK(X1)
MARK(indx(from(x0), y1)) → ACTIVE(indx(active(from(x0)), y1))
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(indx(sel(x0, x1), y1)) → ACTIVE(indx(active(sel(mark(x0), mark(x1))), y1))
MARK(dbl(X)) → MARK(X)
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(dbls(sel(x0, x1))) → ACTIVE(dbls(active(sel(mark(x0), mark(x1)))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbls(from(x0))) → ACTIVE(dbls(active(from(x0))))
MARK(dbls(dbl(x0))) → ACTIVE(dbls(active(dbl(mark(x0)))))
ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
MARK(dbls(0)) → ACTIVE(dbls(active(0)))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(x0)) → ACTIVE(dbls(x0))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
MARK(indx(dbls(x0), y1)) → ACTIVE(indx(active(dbls(mark(x0))), y1))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(dbls(s(x0))) → ACTIVE(dbls(active(s(x0))))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(indx(y0, mark(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(indx(0, y1)) → ACTIVE(indx(active(0), y1))
MARK(indx(y0, active(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(indx(cons(x0, x1), y1)) → ACTIVE(indx(active(cons(x0, x1)), y1))
MARK(dbls(dbls(x0))) → ACTIVE(dbls(active(dbls(mark(x0)))))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(from(X)) → ACTIVE(from(X))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(dbls(cons(x0, x1))) → ACTIVE(dbls(active(cons(x0, x1))))
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(dbls(0)) → ACTIVE(dbls(active(0))) at position [0] we obtained the following new rules:

MARK(dbls(0)) → ACTIVE(dbls(0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ DependencyGraphProof

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(indx(nil, y1)) → ACTIVE(indx(active(nil), y1))
MARK(indx(s(x0), y1)) → ACTIVE(indx(active(s(x0)), y1))
MARK(indx(indx(x0, x1), y1)) → ACTIVE(indx(active(indx(mark(x0), x1)), y1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(indx(dbl(x0), y1)) → ACTIVE(indx(active(dbl(mark(x0))), y1))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(indx(x0, x1)) → ACTIVE(indx(x0, x1))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(dbls(indx(x0, x1))) → ACTIVE(dbls(active(indx(mark(x0), x1))))
MARK(indx(from(x0), y1)) → ACTIVE(indx(active(from(x0)), y1))
MARK(sel(X1, X2)) → MARK(X1)
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(indx(sel(x0, x1), y1)) → ACTIVE(indx(active(sel(mark(x0), mark(x1))), y1))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(dbl(X)) → MARK(X)
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(dbls(sel(x0, x1))) → ACTIVE(dbls(active(sel(mark(x0), mark(x1)))))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbls(from(x0))) → ACTIVE(dbls(active(from(x0))))
MARK(dbls(dbl(x0))) → ACTIVE(dbls(active(dbl(mark(x0)))))
ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(x0)) → ACTIVE(dbls(x0))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(indx(dbls(x0), y1)) → ACTIVE(indx(active(dbls(mark(x0))), y1))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
MARK(dbls(s(x0))) → ACTIVE(dbls(active(s(x0))))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(dbls(0)) → ACTIVE(dbls(0))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(indx(y0, mark(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(y0, active(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(indx(0, y1)) → ACTIVE(indx(active(0), y1))
MARK(indx(cons(x0, x1), y1)) → ACTIVE(indx(active(cons(x0, x1)), y1))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(dbls(dbls(x0))) → ACTIVE(dbls(active(dbls(mark(x0)))))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(from(X)) → ACTIVE(from(X))
MARK(dbls(cons(x0, x1))) → ACTIVE(dbls(active(cons(x0, x1))))
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ DependencyGraphProof

                                                      ↳ QDP

                                                        ↳ Narrowing

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

                                                                ↳ Narrowing

                                                                  ↳ QDP

                                                                    ↳ DependencyGraphProof

                                                                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MARK(indx(X1, X2)) → MARK(X1)
MARK(sel(cons(x0, x1), y1)) → ACTIVE(sel(active(cons(x0, x1)), mark(y1)))
MARK(sel(from(x0), y1)) → ACTIVE(sel(active(from(x0)), mark(y1)))
MARK(indx(nil, y1)) → ACTIVE(indx(active(nil), y1))
MARK(indx(s(x0), y1)) → ACTIVE(indx(active(s(x0)), y1))
MARK(sel(s(x0), y1)) → ACTIVE(sel(active(s(x0)), mark(y1)))
MARK(indx(indx(x0, x1), y1)) → ACTIVE(indx(active(indx(mark(x0), x1)), y1))
ACTIVE(sel(s(X), cons(Y, Z))) → MARK(sel(X, Z))
MARK(sel(y0, indx(x0, x1))) → ACTIVE(sel(mark(y0), active(indx(mark(x0), x1))))
MARK(dbl(sel(x0, x1))) → ACTIVE(dbl(active(sel(mark(x0), mark(x1)))))
MARK(indx(dbl(x0), y1)) → ACTIVE(indx(active(dbl(mark(x0))), y1))
ACTIVE(sel(0, cons(X, Y))) → MARK(X)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(indx(x0, x1)) → ACTIVE(indx(x0, x1))
MARK(dbl(dbl(x0))) → ACTIVE(dbl(active(dbl(mark(x0)))))
MARK(dbls(indx(x0, x1))) → ACTIVE(dbls(active(indx(mark(x0), x1))))
MARK(sel(X1, X2)) → MARK(X1)
MARK(indx(from(x0), y1)) → ACTIVE(indx(active(from(x0)), y1))
MARK(sel(dbl(x0), y1)) → ACTIVE(sel(active(dbl(mark(x0))), mark(y1)))
MARK(dbl(x0)) → ACTIVE(dbl(x0))
MARK(dbl(s(x0))) → ACTIVE(dbl(active(s(x0))))
MARK(indx(sel(x0, x1), y1)) → ACTIVE(indx(active(sel(mark(x0), mark(x1))), y1))
MARK(dbl(X)) → MARK(X)
MARK(dbl(cons(x0, x1))) → ACTIVE(dbl(active(cons(x0, x1))))
MARK(sel(y0, s(x0))) → ACTIVE(sel(mark(y0), active(s(x0))))
MARK(sel(y0, dbl(x0))) → ACTIVE(sel(mark(y0), active(dbl(mark(x0)))))
ACTIVE(dbls(cons(y0, mark(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(dbls(sel(x0, x1))) → ACTIVE(dbls(active(sel(mark(x0), mark(x1)))))
MARK(sel(y0, sel(x0, x1))) → ACTIVE(sel(mark(y0), active(sel(mark(x0), mark(x1)))))
MARK(dbl(from(x0))) → ACTIVE(dbl(active(from(x0))))
MARK(sel(dbls(x0), y1)) → ACTIVE(sel(active(dbls(mark(x0))), mark(y1)))
MARK(dbl(indx(x0, x1))) → ACTIVE(dbl(active(indx(mark(x0), x1))))
MARK(sel(y0, cons(x0, x1))) → ACTIVE(sel(mark(y0), active(cons(x0, x1))))
MARK(dbls(from(x0))) → ACTIVE(dbls(active(from(x0))))
MARK(dbls(dbl(x0))) → ACTIVE(dbls(active(dbl(mark(x0)))))
ACTIVE(dbl(s(active(x0)))) → MARK(s(s(dbl(x0))))
MARK(sel(y0, dbls(x0))) → ACTIVE(sel(mark(y0), active(dbls(mark(x0)))))
MARK(dbl(dbls(x0))) → ACTIVE(dbl(active(dbls(mark(x0)))))
MARK(dbls(x0)) → ACTIVE(dbls(x0))
MARK(dbls(X)) → MARK(X)
ACTIVE(indx(cons(X, Y), Z)) → MARK(cons(sel(X, Z), indx(Y, Z)))
MARK(indx(dbls(x0), y1)) → ACTIVE(indx(active(dbls(mark(x0))), y1))
ACTIVE(dbls(cons(active(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(dbls(s(x0))) → ACTIVE(dbls(active(s(x0))))
MARK(sel(y0, x1)) → ACTIVE(sel(mark(y0), x1))
ACTIVE(dbls(cons(y0, active(x0)))) → MARK(cons(dbl(y0), dbls(x0)))
MARK(sel(0, y1)) → ACTIVE(sel(active(0), mark(y1)))
MARK(sel(y0, 0)) → ACTIVE(sel(mark(y0), active(0)))
ACTIVE(dbls(cons(mark(x0), y1))) → MARK(cons(dbl(x0), dbls(y1)))
MARK(sel(sel(x0, x1), y1)) → ACTIVE(sel(active(sel(mark(x0), mark(x1))), mark(y1)))
MARK(indx(y0, mark(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(sel(indx(x0, x1), y1)) → ACTIVE(sel(active(indx(mark(x0), x1)), mark(y1)))
MARK(indx(0, y1)) → ACTIVE(indx(active(0), y1))
MARK(indx(y0, active(x1))) → ACTIVE(indx(mark(y0), x1))
MARK(sel(x0, y1)) → ACTIVE(sel(x0, mark(y1)))
MARK(indx(cons(x0, x1), y1)) → ACTIVE(indx(active(cons(x0, x1)), y1))
MARK(dbls(dbls(x0))) → ACTIVE(dbls(active(dbls(mark(x0)))))
MARK(sel(y0, from(x0))) → ACTIVE(sel(mark(y0), active(from(x0))))
MARK(from(X)) → ACTIVE(from(X))
MARK(sel(y0, nil)) → ACTIVE(sel(mark(y0), active(nil)))
MARK(sel(nil, y1)) → ACTIVE(sel(active(nil), mark(y1)))
MARK(dbls(cons(x0, x1))) → ACTIVE(dbls(active(cons(x0, x1))))
MARK(sel(X1, X2)) → MARK(X2)
ACTIVE(dbl(s(mark(x0)))) → MARK(s(s(dbl(x0))))

The TRS R consists of the following rules:

active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
mark(dbl(X)) → active(dbl(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(X))
mark(dbls(X)) → active(dbls(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(X1, X2))
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(indx(X1, X2)) → active(indx(mark(X1), X2))
mark(from(X)) → active(from(X))
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
dbls(mark(X)) → dbls(X)
dbls(active(X)) → dbls(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)
indx(mark(X1), X2) → indx(X1, X2)
indx(X1, mark(X2)) → indx(X1, X2)
indx(active(X1), X2) → indx(X1, X2)
indx(X1, active(X2)) → indx(X1, X2)
from(mark(X)) → from(X)
from(active(X)) → from(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.